0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 385 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 27 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 603 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 4 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 51 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
insertC_in_gag(T5, void, tree(T5, void, void)) → insertC_out_gag(T5, void, tree(T5, void, void))
insertC_in_gag(T9, tree(T9, void, void), tree(T9, void, void)) → insertC_out_gag(T9, tree(T9, void, void), tree(T9, void, void))
insertC_in_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U8_gag(T25, T20, pB_in_ga(T25, T20))
pB_in_ga(T25, T20) → U2_ga(T25, T20, lessA_in_g(T25))
lessA_in_g(s(T28)) → U1_g(T28, lessA_in_g(T28))
U1_g(T28, lessA_out_g(T28)) → lessA_out_g(s(T28))
U2_ga(T25, T20, lessA_out_g(T25)) → pB_out_ga(T25, T20)
U2_ga(T25, T20, lessA_out_g(T25)) → U3_ga(T25, T20, insertC_in_gag(s(T25), T20, void))
insertC_in_gag(T39, tree(T39, void, T43), tree(T39, void, void)) → U9_gag(T39, T43, pD_in_ga(T39, T43))
pD_in_ga(T39, T43) → U4_ga(T39, T43, lessA_in_g(T39))
U4_ga(T39, T43, lessA_out_g(T39)) → pD_out_ga(T39, T43)
U4_ga(T39, T43, lessA_out_g(T39)) → U5_ga(T39, T43, insertC_in_gag(T39, T43, void))
insertC_in_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → U10_gag(T57, T54, pB_in_ga(T57, T54))
U10_gag(T57, T54, pB_out_ga(T57, T54)) → insertC_out_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void))
insertC_in_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void)) → U11_gag(T71, T66, pB_in_ga(T71, T66))
U11_gag(T71, T66, pB_out_ga(T71, T66)) → insertC_out_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void))
insertC_in_gag(T80, tree(T80, void, T84), tree(T80, void, void)) → U12_gag(T80, T84, pD_in_ga(T80, T84))
U12_gag(T80, T84, pD_out_ga(T80, T84)) → insertC_out_gag(T80, tree(T80, void, T84), tree(T80, void, void))
insertC_in_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void)) → U13_gag(T96, T93, pB_in_ga(T96, T93))
U13_gag(T96, T93, pB_out_ga(T96, T93)) → insertC_out_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void))
insertC_in_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102)) → insertC_out_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102))
insertC_in_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_gag(T118, T113, T111, T112, lessA_in_g(T118))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → U15_gag(T118, T113, T111, T112, insertC_in_gag(s(T118), T113, T112))
insertC_in_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_gag(T131, T133, T136, T135, lessA_in_g(T131))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → U17_gag(T131, T133, T136, T135, insertC_in_gag(T131, T136, T135))
insertC_in_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_gag(T152, T146, T149, T148, lessA_in_g(T152))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → U19_gag(T152, T146, T149, T148, insertC_in_gag(s(T152), T149, T148))
insertC_in_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → U20_gag(T170, T165, T163, T164, insertC_in_gag(0, T165, T164))
insertC_in_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_gag(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
lessF_in_gg(0, s(T189)) → lessF_out_gg(0, s(T189))
lessF_in_gg(s(0), s(s(T202))) → lessF_out_gg(s(0), s(s(T202)))
lessF_in_gg(s(s(0)), s(s(s(T215)))) → lessF_out_gg(s(s(0)), s(s(s(T215))))
lessF_in_gg(s(s(s(0))), s(s(s(s(T228))))) → lessF_out_gg(s(s(s(0))), s(s(s(s(T228)))))
lessF_in_gg(s(s(s(s(0)))), s(s(s(s(s(T241)))))) → lessF_out_gg(s(s(s(s(0)))), s(s(s(s(s(T241))))))
lessF_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254))))))) → lessF_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254)))))))
lessF_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267)))))))) → lessF_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267))))))))
lessF_in_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_gg(T272, T273, lessE_in_gg(T272, T273))
lessE_in_gg(0, s(T284)) → lessE_out_gg(0, s(T284))
lessE_in_gg(s(T289), s(T290)) → U6_gg(T289, T290, lessE_in_gg(T289, T290))
U6_gg(T289, T290, lessE_out_gg(T289, T290)) → lessE_out_gg(s(T289), s(T290))
U7_gg(T272, T273, lessE_out_gg(T272, T273)) → lessF_out_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273))))))))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → U22_gag(T179, T180, T165, T163, T164, insertC_in_gag(s(T179), T165, T164))
insertC_in_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_gag(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → U24_gag(T305, T306, T307, T310, T309, insertC_in_gag(T305, T310, T309))
insertC_in_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → U25_gag(T332, T324, T327, T326, insertC_in_gag(s(T332), T327, T326))
insertC_in_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_gag(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → U27_gag(T340, T339, T324, T327, T326, insertC_in_gag(s(T340), T327, T326))
U27_gag(T340, T339, T324, T327, T326, insertC_out_gag(s(T340), T327, T326)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U25_gag(T332, T324, T327, T326, insertC_out_gag(s(T332), T327, T326)) → insertC_out_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326))
U24_gag(T305, T306, T307, T310, T309, insertC_out_gag(T305, T310, T309)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U22_gag(T179, T180, T165, T163, T164, insertC_out_gag(s(T179), T165, T164)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U20_gag(T170, T165, T163, T164, insertC_out_gag(0, T165, T164)) → insertC_out_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163))
U19_gag(T152, T146, T149, T148, insertC_out_gag(s(T152), T149, T148)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U17_gag(T131, T133, T136, T135, insertC_out_gag(T131, T136, T135)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U15_gag(T118, T113, T111, T112, insertC_out_gag(s(T118), T113, T112)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U5_ga(T39, T43, insertC_out_gag(T39, T43, void)) → pD_out_ga(T39, T43)
U9_gag(T39, T43, pD_out_ga(T39, T43)) → insertC_out_gag(T39, tree(T39, void, T43), tree(T39, void, void))
U3_ga(T25, T20, insertC_out_gag(s(T25), T20, void)) → pB_out_ga(T25, T20)
U8_gag(T25, T20, pB_out_ga(T25, T20)) → insertC_out_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
insertC_in_gag(T5, void, tree(T5, void, void)) → insertC_out_gag(T5, void, tree(T5, void, void))
insertC_in_gag(T9, tree(T9, void, void), tree(T9, void, void)) → insertC_out_gag(T9, tree(T9, void, void), tree(T9, void, void))
insertC_in_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U8_gag(T25, T20, pB_in_ga(T25, T20))
pB_in_ga(T25, T20) → U2_ga(T25, T20, lessA_in_g(T25))
lessA_in_g(s(T28)) → U1_g(T28, lessA_in_g(T28))
U1_g(T28, lessA_out_g(T28)) → lessA_out_g(s(T28))
U2_ga(T25, T20, lessA_out_g(T25)) → pB_out_ga(T25, T20)
U2_ga(T25, T20, lessA_out_g(T25)) → U3_ga(T25, T20, insertC_in_gag(s(T25), T20, void))
insertC_in_gag(T39, tree(T39, void, T43), tree(T39, void, void)) → U9_gag(T39, T43, pD_in_ga(T39, T43))
pD_in_ga(T39, T43) → U4_ga(T39, T43, lessA_in_g(T39))
U4_ga(T39, T43, lessA_out_g(T39)) → pD_out_ga(T39, T43)
U4_ga(T39, T43, lessA_out_g(T39)) → U5_ga(T39, T43, insertC_in_gag(T39, T43, void))
insertC_in_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → U10_gag(T57, T54, pB_in_ga(T57, T54))
U10_gag(T57, T54, pB_out_ga(T57, T54)) → insertC_out_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void))
insertC_in_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void)) → U11_gag(T71, T66, pB_in_ga(T71, T66))
U11_gag(T71, T66, pB_out_ga(T71, T66)) → insertC_out_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void))
insertC_in_gag(T80, tree(T80, void, T84), tree(T80, void, void)) → U12_gag(T80, T84, pD_in_ga(T80, T84))
U12_gag(T80, T84, pD_out_ga(T80, T84)) → insertC_out_gag(T80, tree(T80, void, T84), tree(T80, void, void))
insertC_in_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void)) → U13_gag(T96, T93, pB_in_ga(T96, T93))
U13_gag(T96, T93, pB_out_ga(T96, T93)) → insertC_out_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void))
insertC_in_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102)) → insertC_out_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102))
insertC_in_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_gag(T118, T113, T111, T112, lessA_in_g(T118))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → U15_gag(T118, T113, T111, T112, insertC_in_gag(s(T118), T113, T112))
insertC_in_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_gag(T131, T133, T136, T135, lessA_in_g(T131))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → U17_gag(T131, T133, T136, T135, insertC_in_gag(T131, T136, T135))
insertC_in_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_gag(T152, T146, T149, T148, lessA_in_g(T152))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → U19_gag(T152, T146, T149, T148, insertC_in_gag(s(T152), T149, T148))
insertC_in_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → U20_gag(T170, T165, T163, T164, insertC_in_gag(0, T165, T164))
insertC_in_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_gag(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
lessF_in_gg(0, s(T189)) → lessF_out_gg(0, s(T189))
lessF_in_gg(s(0), s(s(T202))) → lessF_out_gg(s(0), s(s(T202)))
lessF_in_gg(s(s(0)), s(s(s(T215)))) → lessF_out_gg(s(s(0)), s(s(s(T215))))
lessF_in_gg(s(s(s(0))), s(s(s(s(T228))))) → lessF_out_gg(s(s(s(0))), s(s(s(s(T228)))))
lessF_in_gg(s(s(s(s(0)))), s(s(s(s(s(T241)))))) → lessF_out_gg(s(s(s(s(0)))), s(s(s(s(s(T241))))))
lessF_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254))))))) → lessF_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254)))))))
lessF_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267)))))))) → lessF_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267))))))))
lessF_in_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_gg(T272, T273, lessE_in_gg(T272, T273))
lessE_in_gg(0, s(T284)) → lessE_out_gg(0, s(T284))
lessE_in_gg(s(T289), s(T290)) → U6_gg(T289, T290, lessE_in_gg(T289, T290))
U6_gg(T289, T290, lessE_out_gg(T289, T290)) → lessE_out_gg(s(T289), s(T290))
U7_gg(T272, T273, lessE_out_gg(T272, T273)) → lessF_out_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273))))))))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → U22_gag(T179, T180, T165, T163, T164, insertC_in_gag(s(T179), T165, T164))
insertC_in_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_gag(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → U24_gag(T305, T306, T307, T310, T309, insertC_in_gag(T305, T310, T309))
insertC_in_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → U25_gag(T332, T324, T327, T326, insertC_in_gag(s(T332), T327, T326))
insertC_in_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_gag(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → U27_gag(T340, T339, T324, T327, T326, insertC_in_gag(s(T340), T327, T326))
U27_gag(T340, T339, T324, T327, T326, insertC_out_gag(s(T340), T327, T326)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U25_gag(T332, T324, T327, T326, insertC_out_gag(s(T332), T327, T326)) → insertC_out_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326))
U24_gag(T305, T306, T307, T310, T309, insertC_out_gag(T305, T310, T309)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U22_gag(T179, T180, T165, T163, T164, insertC_out_gag(s(T179), T165, T164)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U20_gag(T170, T165, T163, T164, insertC_out_gag(0, T165, T164)) → insertC_out_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163))
U19_gag(T152, T146, T149, T148, insertC_out_gag(s(T152), T149, T148)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U17_gag(T131, T133, T136, T135, insertC_out_gag(T131, T136, T135)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U15_gag(T118, T113, T111, T112, insertC_out_gag(s(T118), T113, T112)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U5_ga(T39, T43, insertC_out_gag(T39, T43, void)) → pD_out_ga(T39, T43)
U9_gag(T39, T43, pD_out_ga(T39, T43)) → insertC_out_gag(T39, tree(T39, void, T43), tree(T39, void, void))
U3_ga(T25, T20, insertC_out_gag(s(T25), T20, void)) → pB_out_ga(T25, T20)
U8_gag(T25, T20, pB_out_ga(T25, T20)) → insertC_out_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void))
INSERTC_IN_GAG(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U8_GAG(T25, T20, pB_in_ga(T25, T20))
INSERTC_IN_GAG(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → PB_IN_GA(T25, T20)
PB_IN_GA(T25, T20) → U2_GA(T25, T20, lessA_in_g(T25))
PB_IN_GA(T25, T20) → LESSA_IN_G(T25)
LESSA_IN_G(s(T28)) → U1_G(T28, lessA_in_g(T28))
LESSA_IN_G(s(T28)) → LESSA_IN_G(T28)
U2_GA(T25, T20, lessA_out_g(T25)) → U3_GA(T25, T20, insertC_in_gag(s(T25), T20, void))
U2_GA(T25, T20, lessA_out_g(T25)) → INSERTC_IN_GAG(s(T25), T20, void)
INSERTC_IN_GAG(T39, tree(T39, void, T43), tree(T39, void, void)) → U9_GAG(T39, T43, pD_in_ga(T39, T43))
INSERTC_IN_GAG(T39, tree(T39, void, T43), tree(T39, void, void)) → PD_IN_GA(T39, T43)
PD_IN_GA(T39, T43) → U4_GA(T39, T43, lessA_in_g(T39))
PD_IN_GA(T39, T43) → LESSA_IN_G(T39)
U4_GA(T39, T43, lessA_out_g(T39)) → U5_GA(T39, T43, insertC_in_gag(T39, T43, void))
U4_GA(T39, T43, lessA_out_g(T39)) → INSERTC_IN_GAG(T39, T43, void)
INSERTC_IN_GAG(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → U10_GAG(T57, T54, pB_in_ga(T57, T54))
INSERTC_IN_GAG(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → PB_IN_GA(T57, T54)
INSERTC_IN_GAG(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void)) → U11_GAG(T71, T66, pB_in_ga(T71, T66))
INSERTC_IN_GAG(T80, tree(T80, void, T84), tree(T80, void, void)) → U12_GAG(T80, T84, pD_in_ga(T80, T84))
INSERTC_IN_GAG(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void)) → U13_GAG(T96, T93, pB_in_ga(T96, T93))
INSERTC_IN_GAG(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_GAG(T118, T113, T111, T112, lessA_in_g(T118))
INSERTC_IN_GAG(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → LESSA_IN_G(T118)
U14_GAG(T118, T113, T111, T112, lessA_out_g(T118)) → U15_GAG(T118, T113, T111, T112, insertC_in_gag(s(T118), T113, T112))
U14_GAG(T118, T113, T111, T112, lessA_out_g(T118)) → INSERTC_IN_GAG(s(T118), T113, T112)
INSERTC_IN_GAG(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_GAG(T131, T133, T136, T135, lessA_in_g(T131))
INSERTC_IN_GAG(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → LESSA_IN_G(T131)
U16_GAG(T131, T133, T136, T135, lessA_out_g(T131)) → U17_GAG(T131, T133, T136, T135, insertC_in_gag(T131, T136, T135))
U16_GAG(T131, T133, T136, T135, lessA_out_g(T131)) → INSERTC_IN_GAG(T131, T136, T135)
INSERTC_IN_GAG(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_GAG(T152, T146, T149, T148, lessA_in_g(T152))
INSERTC_IN_GAG(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → LESSA_IN_G(T152)
U18_GAG(T152, T146, T149, T148, lessA_out_g(T152)) → U19_GAG(T152, T146, T149, T148, insertC_in_gag(s(T152), T149, T148))
U18_GAG(T152, T146, T149, T148, lessA_out_g(T152)) → INSERTC_IN_GAG(s(T152), T149, T148)
INSERTC_IN_GAG(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → U20_GAG(T170, T165, T163, T164, insertC_in_gag(0, T165, T164))
INSERTC_IN_GAG(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → INSERTC_IN_GAG(0, T165, T164)
INSERTC_IN_GAG(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_GAG(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
INSERTC_IN_GAG(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → LESSF_IN_GG(T179, T180)
LESSF_IN_GG(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_GG(T272, T273, lessE_in_gg(T272, T273))
LESSF_IN_GG(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → LESSE_IN_GG(T272, T273)
LESSE_IN_GG(s(T289), s(T290)) → U6_GG(T289, T290, lessE_in_gg(T289, T290))
LESSE_IN_GG(s(T289), s(T290)) → LESSE_IN_GG(T289, T290)
U21_GAG(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → U22_GAG(T179, T180, T165, T163, T164, insertC_in_gag(s(T179), T165, T164))
U21_GAG(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → INSERTC_IN_GAG(s(T179), T165, T164)
INSERTC_IN_GAG(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_GAG(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
INSERTC_IN_GAG(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → LESSE_IN_GG(T306, T305)
U23_GAG(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → U24_GAG(T305, T306, T307, T310, T309, insertC_in_gag(T305, T310, T309))
U23_GAG(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → INSERTC_IN_GAG(T305, T310, T309)
INSERTC_IN_GAG(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → U25_GAG(T332, T324, T327, T326, insertC_in_gag(s(T332), T327, T326))
INSERTC_IN_GAG(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → INSERTC_IN_GAG(s(T332), T327, T326)
INSERTC_IN_GAG(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_GAG(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
INSERTC_IN_GAG(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → LESSE_IN_GG(T339, T340)
U26_GAG(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → U27_GAG(T340, T339, T324, T327, T326, insertC_in_gag(s(T340), T327, T326))
U26_GAG(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → INSERTC_IN_GAG(s(T340), T327, T326)
insertC_in_gag(T5, void, tree(T5, void, void)) → insertC_out_gag(T5, void, tree(T5, void, void))
insertC_in_gag(T9, tree(T9, void, void), tree(T9, void, void)) → insertC_out_gag(T9, tree(T9, void, void), tree(T9, void, void))
insertC_in_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U8_gag(T25, T20, pB_in_ga(T25, T20))
pB_in_ga(T25, T20) → U2_ga(T25, T20, lessA_in_g(T25))
lessA_in_g(s(T28)) → U1_g(T28, lessA_in_g(T28))
U1_g(T28, lessA_out_g(T28)) → lessA_out_g(s(T28))
U2_ga(T25, T20, lessA_out_g(T25)) → pB_out_ga(T25, T20)
U2_ga(T25, T20, lessA_out_g(T25)) → U3_ga(T25, T20, insertC_in_gag(s(T25), T20, void))
insertC_in_gag(T39, tree(T39, void, T43), tree(T39, void, void)) → U9_gag(T39, T43, pD_in_ga(T39, T43))
pD_in_ga(T39, T43) → U4_ga(T39, T43, lessA_in_g(T39))
U4_ga(T39, T43, lessA_out_g(T39)) → pD_out_ga(T39, T43)
U4_ga(T39, T43, lessA_out_g(T39)) → U5_ga(T39, T43, insertC_in_gag(T39, T43, void))
insertC_in_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → U10_gag(T57, T54, pB_in_ga(T57, T54))
U10_gag(T57, T54, pB_out_ga(T57, T54)) → insertC_out_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void))
insertC_in_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void)) → U11_gag(T71, T66, pB_in_ga(T71, T66))
U11_gag(T71, T66, pB_out_ga(T71, T66)) → insertC_out_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void))
insertC_in_gag(T80, tree(T80, void, T84), tree(T80, void, void)) → U12_gag(T80, T84, pD_in_ga(T80, T84))
U12_gag(T80, T84, pD_out_ga(T80, T84)) → insertC_out_gag(T80, tree(T80, void, T84), tree(T80, void, void))
insertC_in_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void)) → U13_gag(T96, T93, pB_in_ga(T96, T93))
U13_gag(T96, T93, pB_out_ga(T96, T93)) → insertC_out_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void))
insertC_in_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102)) → insertC_out_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102))
insertC_in_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_gag(T118, T113, T111, T112, lessA_in_g(T118))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → U15_gag(T118, T113, T111, T112, insertC_in_gag(s(T118), T113, T112))
insertC_in_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_gag(T131, T133, T136, T135, lessA_in_g(T131))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → U17_gag(T131, T133, T136, T135, insertC_in_gag(T131, T136, T135))
insertC_in_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_gag(T152, T146, T149, T148, lessA_in_g(T152))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → U19_gag(T152, T146, T149, T148, insertC_in_gag(s(T152), T149, T148))
insertC_in_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → U20_gag(T170, T165, T163, T164, insertC_in_gag(0, T165, T164))
insertC_in_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_gag(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
lessF_in_gg(0, s(T189)) → lessF_out_gg(0, s(T189))
lessF_in_gg(s(0), s(s(T202))) → lessF_out_gg(s(0), s(s(T202)))
lessF_in_gg(s(s(0)), s(s(s(T215)))) → lessF_out_gg(s(s(0)), s(s(s(T215))))
lessF_in_gg(s(s(s(0))), s(s(s(s(T228))))) → lessF_out_gg(s(s(s(0))), s(s(s(s(T228)))))
lessF_in_gg(s(s(s(s(0)))), s(s(s(s(s(T241)))))) → lessF_out_gg(s(s(s(s(0)))), s(s(s(s(s(T241))))))
lessF_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254))))))) → lessF_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254)))))))
lessF_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267)))))))) → lessF_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267))))))))
lessF_in_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_gg(T272, T273, lessE_in_gg(T272, T273))
lessE_in_gg(0, s(T284)) → lessE_out_gg(0, s(T284))
lessE_in_gg(s(T289), s(T290)) → U6_gg(T289, T290, lessE_in_gg(T289, T290))
U6_gg(T289, T290, lessE_out_gg(T289, T290)) → lessE_out_gg(s(T289), s(T290))
U7_gg(T272, T273, lessE_out_gg(T272, T273)) → lessF_out_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273))))))))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → U22_gag(T179, T180, T165, T163, T164, insertC_in_gag(s(T179), T165, T164))
insertC_in_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_gag(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → U24_gag(T305, T306, T307, T310, T309, insertC_in_gag(T305, T310, T309))
insertC_in_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → U25_gag(T332, T324, T327, T326, insertC_in_gag(s(T332), T327, T326))
insertC_in_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_gag(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → U27_gag(T340, T339, T324, T327, T326, insertC_in_gag(s(T340), T327, T326))
U27_gag(T340, T339, T324, T327, T326, insertC_out_gag(s(T340), T327, T326)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U25_gag(T332, T324, T327, T326, insertC_out_gag(s(T332), T327, T326)) → insertC_out_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326))
U24_gag(T305, T306, T307, T310, T309, insertC_out_gag(T305, T310, T309)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U22_gag(T179, T180, T165, T163, T164, insertC_out_gag(s(T179), T165, T164)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U20_gag(T170, T165, T163, T164, insertC_out_gag(0, T165, T164)) → insertC_out_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163))
U19_gag(T152, T146, T149, T148, insertC_out_gag(s(T152), T149, T148)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U17_gag(T131, T133, T136, T135, insertC_out_gag(T131, T136, T135)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U15_gag(T118, T113, T111, T112, insertC_out_gag(s(T118), T113, T112)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U5_ga(T39, T43, insertC_out_gag(T39, T43, void)) → pD_out_ga(T39, T43)
U9_gag(T39, T43, pD_out_ga(T39, T43)) → insertC_out_gag(T39, tree(T39, void, T43), tree(T39, void, void))
U3_ga(T25, T20, insertC_out_gag(s(T25), T20, void)) → pB_out_ga(T25, T20)
U8_gag(T25, T20, pB_out_ga(T25, T20)) → insertC_out_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void))
INSERTC_IN_GAG(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U8_GAG(T25, T20, pB_in_ga(T25, T20))
INSERTC_IN_GAG(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → PB_IN_GA(T25, T20)
PB_IN_GA(T25, T20) → U2_GA(T25, T20, lessA_in_g(T25))
PB_IN_GA(T25, T20) → LESSA_IN_G(T25)
LESSA_IN_G(s(T28)) → U1_G(T28, lessA_in_g(T28))
LESSA_IN_G(s(T28)) → LESSA_IN_G(T28)
U2_GA(T25, T20, lessA_out_g(T25)) → U3_GA(T25, T20, insertC_in_gag(s(T25), T20, void))
U2_GA(T25, T20, lessA_out_g(T25)) → INSERTC_IN_GAG(s(T25), T20, void)
INSERTC_IN_GAG(T39, tree(T39, void, T43), tree(T39, void, void)) → U9_GAG(T39, T43, pD_in_ga(T39, T43))
INSERTC_IN_GAG(T39, tree(T39, void, T43), tree(T39, void, void)) → PD_IN_GA(T39, T43)
PD_IN_GA(T39, T43) → U4_GA(T39, T43, lessA_in_g(T39))
PD_IN_GA(T39, T43) → LESSA_IN_G(T39)
U4_GA(T39, T43, lessA_out_g(T39)) → U5_GA(T39, T43, insertC_in_gag(T39, T43, void))
U4_GA(T39, T43, lessA_out_g(T39)) → INSERTC_IN_GAG(T39, T43, void)
INSERTC_IN_GAG(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → U10_GAG(T57, T54, pB_in_ga(T57, T54))
INSERTC_IN_GAG(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → PB_IN_GA(T57, T54)
INSERTC_IN_GAG(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void)) → U11_GAG(T71, T66, pB_in_ga(T71, T66))
INSERTC_IN_GAG(T80, tree(T80, void, T84), tree(T80, void, void)) → U12_GAG(T80, T84, pD_in_ga(T80, T84))
INSERTC_IN_GAG(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void)) → U13_GAG(T96, T93, pB_in_ga(T96, T93))
INSERTC_IN_GAG(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_GAG(T118, T113, T111, T112, lessA_in_g(T118))
INSERTC_IN_GAG(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → LESSA_IN_G(T118)
U14_GAG(T118, T113, T111, T112, lessA_out_g(T118)) → U15_GAG(T118, T113, T111, T112, insertC_in_gag(s(T118), T113, T112))
U14_GAG(T118, T113, T111, T112, lessA_out_g(T118)) → INSERTC_IN_GAG(s(T118), T113, T112)
INSERTC_IN_GAG(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_GAG(T131, T133, T136, T135, lessA_in_g(T131))
INSERTC_IN_GAG(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → LESSA_IN_G(T131)
U16_GAG(T131, T133, T136, T135, lessA_out_g(T131)) → U17_GAG(T131, T133, T136, T135, insertC_in_gag(T131, T136, T135))
U16_GAG(T131, T133, T136, T135, lessA_out_g(T131)) → INSERTC_IN_GAG(T131, T136, T135)
INSERTC_IN_GAG(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_GAG(T152, T146, T149, T148, lessA_in_g(T152))
INSERTC_IN_GAG(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → LESSA_IN_G(T152)
U18_GAG(T152, T146, T149, T148, lessA_out_g(T152)) → U19_GAG(T152, T146, T149, T148, insertC_in_gag(s(T152), T149, T148))
U18_GAG(T152, T146, T149, T148, lessA_out_g(T152)) → INSERTC_IN_GAG(s(T152), T149, T148)
INSERTC_IN_GAG(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → U20_GAG(T170, T165, T163, T164, insertC_in_gag(0, T165, T164))
INSERTC_IN_GAG(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → INSERTC_IN_GAG(0, T165, T164)
INSERTC_IN_GAG(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_GAG(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
INSERTC_IN_GAG(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → LESSF_IN_GG(T179, T180)
LESSF_IN_GG(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_GG(T272, T273, lessE_in_gg(T272, T273))
LESSF_IN_GG(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → LESSE_IN_GG(T272, T273)
LESSE_IN_GG(s(T289), s(T290)) → U6_GG(T289, T290, lessE_in_gg(T289, T290))
LESSE_IN_GG(s(T289), s(T290)) → LESSE_IN_GG(T289, T290)
U21_GAG(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → U22_GAG(T179, T180, T165, T163, T164, insertC_in_gag(s(T179), T165, T164))
U21_GAG(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → INSERTC_IN_GAG(s(T179), T165, T164)
INSERTC_IN_GAG(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_GAG(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
INSERTC_IN_GAG(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → LESSE_IN_GG(T306, T305)
U23_GAG(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → U24_GAG(T305, T306, T307, T310, T309, insertC_in_gag(T305, T310, T309))
U23_GAG(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → INSERTC_IN_GAG(T305, T310, T309)
INSERTC_IN_GAG(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → U25_GAG(T332, T324, T327, T326, insertC_in_gag(s(T332), T327, T326))
INSERTC_IN_GAG(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → INSERTC_IN_GAG(s(T332), T327, T326)
INSERTC_IN_GAG(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_GAG(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
INSERTC_IN_GAG(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → LESSE_IN_GG(T339, T340)
U26_GAG(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → U27_GAG(T340, T339, T324, T327, T326, insertC_in_gag(s(T340), T327, T326))
U26_GAG(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → INSERTC_IN_GAG(s(T340), T327, T326)
insertC_in_gag(T5, void, tree(T5, void, void)) → insertC_out_gag(T5, void, tree(T5, void, void))
insertC_in_gag(T9, tree(T9, void, void), tree(T9, void, void)) → insertC_out_gag(T9, tree(T9, void, void), tree(T9, void, void))
insertC_in_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U8_gag(T25, T20, pB_in_ga(T25, T20))
pB_in_ga(T25, T20) → U2_ga(T25, T20, lessA_in_g(T25))
lessA_in_g(s(T28)) → U1_g(T28, lessA_in_g(T28))
U1_g(T28, lessA_out_g(T28)) → lessA_out_g(s(T28))
U2_ga(T25, T20, lessA_out_g(T25)) → pB_out_ga(T25, T20)
U2_ga(T25, T20, lessA_out_g(T25)) → U3_ga(T25, T20, insertC_in_gag(s(T25), T20, void))
insertC_in_gag(T39, tree(T39, void, T43), tree(T39, void, void)) → U9_gag(T39, T43, pD_in_ga(T39, T43))
pD_in_ga(T39, T43) → U4_ga(T39, T43, lessA_in_g(T39))
U4_ga(T39, T43, lessA_out_g(T39)) → pD_out_ga(T39, T43)
U4_ga(T39, T43, lessA_out_g(T39)) → U5_ga(T39, T43, insertC_in_gag(T39, T43, void))
insertC_in_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → U10_gag(T57, T54, pB_in_ga(T57, T54))
U10_gag(T57, T54, pB_out_ga(T57, T54)) → insertC_out_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void))
insertC_in_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void)) → U11_gag(T71, T66, pB_in_ga(T71, T66))
U11_gag(T71, T66, pB_out_ga(T71, T66)) → insertC_out_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void))
insertC_in_gag(T80, tree(T80, void, T84), tree(T80, void, void)) → U12_gag(T80, T84, pD_in_ga(T80, T84))
U12_gag(T80, T84, pD_out_ga(T80, T84)) → insertC_out_gag(T80, tree(T80, void, T84), tree(T80, void, void))
insertC_in_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void)) → U13_gag(T96, T93, pB_in_ga(T96, T93))
U13_gag(T96, T93, pB_out_ga(T96, T93)) → insertC_out_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void))
insertC_in_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102)) → insertC_out_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102))
insertC_in_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_gag(T118, T113, T111, T112, lessA_in_g(T118))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → U15_gag(T118, T113, T111, T112, insertC_in_gag(s(T118), T113, T112))
insertC_in_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_gag(T131, T133, T136, T135, lessA_in_g(T131))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → U17_gag(T131, T133, T136, T135, insertC_in_gag(T131, T136, T135))
insertC_in_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_gag(T152, T146, T149, T148, lessA_in_g(T152))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → U19_gag(T152, T146, T149, T148, insertC_in_gag(s(T152), T149, T148))
insertC_in_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → U20_gag(T170, T165, T163, T164, insertC_in_gag(0, T165, T164))
insertC_in_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_gag(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
lessF_in_gg(0, s(T189)) → lessF_out_gg(0, s(T189))
lessF_in_gg(s(0), s(s(T202))) → lessF_out_gg(s(0), s(s(T202)))
lessF_in_gg(s(s(0)), s(s(s(T215)))) → lessF_out_gg(s(s(0)), s(s(s(T215))))
lessF_in_gg(s(s(s(0))), s(s(s(s(T228))))) → lessF_out_gg(s(s(s(0))), s(s(s(s(T228)))))
lessF_in_gg(s(s(s(s(0)))), s(s(s(s(s(T241)))))) → lessF_out_gg(s(s(s(s(0)))), s(s(s(s(s(T241))))))
lessF_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254))))))) → lessF_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254)))))))
lessF_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267)))))))) → lessF_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267))))))))
lessF_in_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_gg(T272, T273, lessE_in_gg(T272, T273))
lessE_in_gg(0, s(T284)) → lessE_out_gg(0, s(T284))
lessE_in_gg(s(T289), s(T290)) → U6_gg(T289, T290, lessE_in_gg(T289, T290))
U6_gg(T289, T290, lessE_out_gg(T289, T290)) → lessE_out_gg(s(T289), s(T290))
U7_gg(T272, T273, lessE_out_gg(T272, T273)) → lessF_out_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273))))))))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → U22_gag(T179, T180, T165, T163, T164, insertC_in_gag(s(T179), T165, T164))
insertC_in_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_gag(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → U24_gag(T305, T306, T307, T310, T309, insertC_in_gag(T305, T310, T309))
insertC_in_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → U25_gag(T332, T324, T327, T326, insertC_in_gag(s(T332), T327, T326))
insertC_in_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_gag(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → U27_gag(T340, T339, T324, T327, T326, insertC_in_gag(s(T340), T327, T326))
U27_gag(T340, T339, T324, T327, T326, insertC_out_gag(s(T340), T327, T326)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U25_gag(T332, T324, T327, T326, insertC_out_gag(s(T332), T327, T326)) → insertC_out_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326))
U24_gag(T305, T306, T307, T310, T309, insertC_out_gag(T305, T310, T309)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U22_gag(T179, T180, T165, T163, T164, insertC_out_gag(s(T179), T165, T164)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U20_gag(T170, T165, T163, T164, insertC_out_gag(0, T165, T164)) → insertC_out_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163))
U19_gag(T152, T146, T149, T148, insertC_out_gag(s(T152), T149, T148)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U17_gag(T131, T133, T136, T135, insertC_out_gag(T131, T136, T135)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U15_gag(T118, T113, T111, T112, insertC_out_gag(s(T118), T113, T112)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U5_ga(T39, T43, insertC_out_gag(T39, T43, void)) → pD_out_ga(T39, T43)
U9_gag(T39, T43, pD_out_ga(T39, T43)) → insertC_out_gag(T39, tree(T39, void, T43), tree(T39, void, void))
U3_ga(T25, T20, insertC_out_gag(s(T25), T20, void)) → pB_out_ga(T25, T20)
U8_gag(T25, T20, pB_out_ga(T25, T20)) → insertC_out_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void))
LESSE_IN_GG(s(T289), s(T290)) → LESSE_IN_GG(T289, T290)
insertC_in_gag(T5, void, tree(T5, void, void)) → insertC_out_gag(T5, void, tree(T5, void, void))
insertC_in_gag(T9, tree(T9, void, void), tree(T9, void, void)) → insertC_out_gag(T9, tree(T9, void, void), tree(T9, void, void))
insertC_in_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U8_gag(T25, T20, pB_in_ga(T25, T20))
pB_in_ga(T25, T20) → U2_ga(T25, T20, lessA_in_g(T25))
lessA_in_g(s(T28)) → U1_g(T28, lessA_in_g(T28))
U1_g(T28, lessA_out_g(T28)) → lessA_out_g(s(T28))
U2_ga(T25, T20, lessA_out_g(T25)) → pB_out_ga(T25, T20)
U2_ga(T25, T20, lessA_out_g(T25)) → U3_ga(T25, T20, insertC_in_gag(s(T25), T20, void))
insertC_in_gag(T39, tree(T39, void, T43), tree(T39, void, void)) → U9_gag(T39, T43, pD_in_ga(T39, T43))
pD_in_ga(T39, T43) → U4_ga(T39, T43, lessA_in_g(T39))
U4_ga(T39, T43, lessA_out_g(T39)) → pD_out_ga(T39, T43)
U4_ga(T39, T43, lessA_out_g(T39)) → U5_ga(T39, T43, insertC_in_gag(T39, T43, void))
insertC_in_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → U10_gag(T57, T54, pB_in_ga(T57, T54))
U10_gag(T57, T54, pB_out_ga(T57, T54)) → insertC_out_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void))
insertC_in_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void)) → U11_gag(T71, T66, pB_in_ga(T71, T66))
U11_gag(T71, T66, pB_out_ga(T71, T66)) → insertC_out_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void))
insertC_in_gag(T80, tree(T80, void, T84), tree(T80, void, void)) → U12_gag(T80, T84, pD_in_ga(T80, T84))
U12_gag(T80, T84, pD_out_ga(T80, T84)) → insertC_out_gag(T80, tree(T80, void, T84), tree(T80, void, void))
insertC_in_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void)) → U13_gag(T96, T93, pB_in_ga(T96, T93))
U13_gag(T96, T93, pB_out_ga(T96, T93)) → insertC_out_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void))
insertC_in_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102)) → insertC_out_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102))
insertC_in_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_gag(T118, T113, T111, T112, lessA_in_g(T118))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → U15_gag(T118, T113, T111, T112, insertC_in_gag(s(T118), T113, T112))
insertC_in_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_gag(T131, T133, T136, T135, lessA_in_g(T131))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → U17_gag(T131, T133, T136, T135, insertC_in_gag(T131, T136, T135))
insertC_in_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_gag(T152, T146, T149, T148, lessA_in_g(T152))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → U19_gag(T152, T146, T149, T148, insertC_in_gag(s(T152), T149, T148))
insertC_in_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → U20_gag(T170, T165, T163, T164, insertC_in_gag(0, T165, T164))
insertC_in_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_gag(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
lessF_in_gg(0, s(T189)) → lessF_out_gg(0, s(T189))
lessF_in_gg(s(0), s(s(T202))) → lessF_out_gg(s(0), s(s(T202)))
lessF_in_gg(s(s(0)), s(s(s(T215)))) → lessF_out_gg(s(s(0)), s(s(s(T215))))
lessF_in_gg(s(s(s(0))), s(s(s(s(T228))))) → lessF_out_gg(s(s(s(0))), s(s(s(s(T228)))))
lessF_in_gg(s(s(s(s(0)))), s(s(s(s(s(T241)))))) → lessF_out_gg(s(s(s(s(0)))), s(s(s(s(s(T241))))))
lessF_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254))))))) → lessF_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254)))))))
lessF_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267)))))))) → lessF_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267))))))))
lessF_in_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_gg(T272, T273, lessE_in_gg(T272, T273))
lessE_in_gg(0, s(T284)) → lessE_out_gg(0, s(T284))
lessE_in_gg(s(T289), s(T290)) → U6_gg(T289, T290, lessE_in_gg(T289, T290))
U6_gg(T289, T290, lessE_out_gg(T289, T290)) → lessE_out_gg(s(T289), s(T290))
U7_gg(T272, T273, lessE_out_gg(T272, T273)) → lessF_out_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273))))))))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → U22_gag(T179, T180, T165, T163, T164, insertC_in_gag(s(T179), T165, T164))
insertC_in_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_gag(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → U24_gag(T305, T306, T307, T310, T309, insertC_in_gag(T305, T310, T309))
insertC_in_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → U25_gag(T332, T324, T327, T326, insertC_in_gag(s(T332), T327, T326))
insertC_in_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_gag(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → U27_gag(T340, T339, T324, T327, T326, insertC_in_gag(s(T340), T327, T326))
U27_gag(T340, T339, T324, T327, T326, insertC_out_gag(s(T340), T327, T326)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U25_gag(T332, T324, T327, T326, insertC_out_gag(s(T332), T327, T326)) → insertC_out_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326))
U24_gag(T305, T306, T307, T310, T309, insertC_out_gag(T305, T310, T309)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U22_gag(T179, T180, T165, T163, T164, insertC_out_gag(s(T179), T165, T164)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U20_gag(T170, T165, T163, T164, insertC_out_gag(0, T165, T164)) → insertC_out_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163))
U19_gag(T152, T146, T149, T148, insertC_out_gag(s(T152), T149, T148)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U17_gag(T131, T133, T136, T135, insertC_out_gag(T131, T136, T135)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U15_gag(T118, T113, T111, T112, insertC_out_gag(s(T118), T113, T112)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U5_ga(T39, T43, insertC_out_gag(T39, T43, void)) → pD_out_ga(T39, T43)
U9_gag(T39, T43, pD_out_ga(T39, T43)) → insertC_out_gag(T39, tree(T39, void, T43), tree(T39, void, void))
U3_ga(T25, T20, insertC_out_gag(s(T25), T20, void)) → pB_out_ga(T25, T20)
U8_gag(T25, T20, pB_out_ga(T25, T20)) → insertC_out_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void))
LESSE_IN_GG(s(T289), s(T290)) → LESSE_IN_GG(T289, T290)
LESSE_IN_GG(s(T289), s(T290)) → LESSE_IN_GG(T289, T290)
From the DPs we obtained the following set of size-change graphs:
LESSA_IN_G(s(T28)) → LESSA_IN_G(T28)
insertC_in_gag(T5, void, tree(T5, void, void)) → insertC_out_gag(T5, void, tree(T5, void, void))
insertC_in_gag(T9, tree(T9, void, void), tree(T9, void, void)) → insertC_out_gag(T9, tree(T9, void, void), tree(T9, void, void))
insertC_in_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U8_gag(T25, T20, pB_in_ga(T25, T20))
pB_in_ga(T25, T20) → U2_ga(T25, T20, lessA_in_g(T25))
lessA_in_g(s(T28)) → U1_g(T28, lessA_in_g(T28))
U1_g(T28, lessA_out_g(T28)) → lessA_out_g(s(T28))
U2_ga(T25, T20, lessA_out_g(T25)) → pB_out_ga(T25, T20)
U2_ga(T25, T20, lessA_out_g(T25)) → U3_ga(T25, T20, insertC_in_gag(s(T25), T20, void))
insertC_in_gag(T39, tree(T39, void, T43), tree(T39, void, void)) → U9_gag(T39, T43, pD_in_ga(T39, T43))
pD_in_ga(T39, T43) → U4_ga(T39, T43, lessA_in_g(T39))
U4_ga(T39, T43, lessA_out_g(T39)) → pD_out_ga(T39, T43)
U4_ga(T39, T43, lessA_out_g(T39)) → U5_ga(T39, T43, insertC_in_gag(T39, T43, void))
insertC_in_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → U10_gag(T57, T54, pB_in_ga(T57, T54))
U10_gag(T57, T54, pB_out_ga(T57, T54)) → insertC_out_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void))
insertC_in_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void)) → U11_gag(T71, T66, pB_in_ga(T71, T66))
U11_gag(T71, T66, pB_out_ga(T71, T66)) → insertC_out_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void))
insertC_in_gag(T80, tree(T80, void, T84), tree(T80, void, void)) → U12_gag(T80, T84, pD_in_ga(T80, T84))
U12_gag(T80, T84, pD_out_ga(T80, T84)) → insertC_out_gag(T80, tree(T80, void, T84), tree(T80, void, void))
insertC_in_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void)) → U13_gag(T96, T93, pB_in_ga(T96, T93))
U13_gag(T96, T93, pB_out_ga(T96, T93)) → insertC_out_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void))
insertC_in_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102)) → insertC_out_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102))
insertC_in_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_gag(T118, T113, T111, T112, lessA_in_g(T118))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → U15_gag(T118, T113, T111, T112, insertC_in_gag(s(T118), T113, T112))
insertC_in_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_gag(T131, T133, T136, T135, lessA_in_g(T131))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → U17_gag(T131, T133, T136, T135, insertC_in_gag(T131, T136, T135))
insertC_in_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_gag(T152, T146, T149, T148, lessA_in_g(T152))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → U19_gag(T152, T146, T149, T148, insertC_in_gag(s(T152), T149, T148))
insertC_in_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → U20_gag(T170, T165, T163, T164, insertC_in_gag(0, T165, T164))
insertC_in_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_gag(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
lessF_in_gg(0, s(T189)) → lessF_out_gg(0, s(T189))
lessF_in_gg(s(0), s(s(T202))) → lessF_out_gg(s(0), s(s(T202)))
lessF_in_gg(s(s(0)), s(s(s(T215)))) → lessF_out_gg(s(s(0)), s(s(s(T215))))
lessF_in_gg(s(s(s(0))), s(s(s(s(T228))))) → lessF_out_gg(s(s(s(0))), s(s(s(s(T228)))))
lessF_in_gg(s(s(s(s(0)))), s(s(s(s(s(T241)))))) → lessF_out_gg(s(s(s(s(0)))), s(s(s(s(s(T241))))))
lessF_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254))))))) → lessF_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254)))))))
lessF_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267)))))))) → lessF_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267))))))))
lessF_in_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_gg(T272, T273, lessE_in_gg(T272, T273))
lessE_in_gg(0, s(T284)) → lessE_out_gg(0, s(T284))
lessE_in_gg(s(T289), s(T290)) → U6_gg(T289, T290, lessE_in_gg(T289, T290))
U6_gg(T289, T290, lessE_out_gg(T289, T290)) → lessE_out_gg(s(T289), s(T290))
U7_gg(T272, T273, lessE_out_gg(T272, T273)) → lessF_out_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273))))))))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → U22_gag(T179, T180, T165, T163, T164, insertC_in_gag(s(T179), T165, T164))
insertC_in_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_gag(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → U24_gag(T305, T306, T307, T310, T309, insertC_in_gag(T305, T310, T309))
insertC_in_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → U25_gag(T332, T324, T327, T326, insertC_in_gag(s(T332), T327, T326))
insertC_in_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_gag(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → U27_gag(T340, T339, T324, T327, T326, insertC_in_gag(s(T340), T327, T326))
U27_gag(T340, T339, T324, T327, T326, insertC_out_gag(s(T340), T327, T326)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U25_gag(T332, T324, T327, T326, insertC_out_gag(s(T332), T327, T326)) → insertC_out_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326))
U24_gag(T305, T306, T307, T310, T309, insertC_out_gag(T305, T310, T309)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U22_gag(T179, T180, T165, T163, T164, insertC_out_gag(s(T179), T165, T164)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U20_gag(T170, T165, T163, T164, insertC_out_gag(0, T165, T164)) → insertC_out_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163))
U19_gag(T152, T146, T149, T148, insertC_out_gag(s(T152), T149, T148)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U17_gag(T131, T133, T136, T135, insertC_out_gag(T131, T136, T135)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U15_gag(T118, T113, T111, T112, insertC_out_gag(s(T118), T113, T112)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U5_ga(T39, T43, insertC_out_gag(T39, T43, void)) → pD_out_ga(T39, T43)
U9_gag(T39, T43, pD_out_ga(T39, T43)) → insertC_out_gag(T39, tree(T39, void, T43), tree(T39, void, void))
U3_ga(T25, T20, insertC_out_gag(s(T25), T20, void)) → pB_out_ga(T25, T20)
U8_gag(T25, T20, pB_out_ga(T25, T20)) → insertC_out_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void))
LESSA_IN_G(s(T28)) → LESSA_IN_G(T28)
LESSA_IN_G(s(T28)) → LESSA_IN_G(T28)
From the DPs we obtained the following set of size-change graphs:
INSERTC_IN_GAG(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_GAG(T118, T113, T111, T112, lessA_in_g(T118))
U14_GAG(T118, T113, T111, T112, lessA_out_g(T118)) → INSERTC_IN_GAG(s(T118), T113, T112)
INSERTC_IN_GAG(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_GAG(T131, T133, T136, T135, lessA_in_g(T131))
U16_GAG(T131, T133, T136, T135, lessA_out_g(T131)) → INSERTC_IN_GAG(T131, T136, T135)
INSERTC_IN_GAG(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_GAG(T152, T146, T149, T148, lessA_in_g(T152))
U18_GAG(T152, T146, T149, T148, lessA_out_g(T152)) → INSERTC_IN_GAG(s(T152), T149, T148)
INSERTC_IN_GAG(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_GAG(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
U21_GAG(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → INSERTC_IN_GAG(s(T179), T165, T164)
INSERTC_IN_GAG(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_GAG(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
U23_GAG(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → INSERTC_IN_GAG(T305, T310, T309)
INSERTC_IN_GAG(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → INSERTC_IN_GAG(0, T165, T164)
INSERTC_IN_GAG(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → INSERTC_IN_GAG(s(T332), T327, T326)
INSERTC_IN_GAG(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_GAG(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
U26_GAG(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → INSERTC_IN_GAG(s(T340), T327, T326)
insertC_in_gag(T5, void, tree(T5, void, void)) → insertC_out_gag(T5, void, tree(T5, void, void))
insertC_in_gag(T9, tree(T9, void, void), tree(T9, void, void)) → insertC_out_gag(T9, tree(T9, void, void), tree(T9, void, void))
insertC_in_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void)) → U8_gag(T25, T20, pB_in_ga(T25, T20))
pB_in_ga(T25, T20) → U2_ga(T25, T20, lessA_in_g(T25))
lessA_in_g(s(T28)) → U1_g(T28, lessA_in_g(T28))
U1_g(T28, lessA_out_g(T28)) → lessA_out_g(s(T28))
U2_ga(T25, T20, lessA_out_g(T25)) → pB_out_ga(T25, T20)
U2_ga(T25, T20, lessA_out_g(T25)) → U3_ga(T25, T20, insertC_in_gag(s(T25), T20, void))
insertC_in_gag(T39, tree(T39, void, T43), tree(T39, void, void)) → U9_gag(T39, T43, pD_in_ga(T39, T43))
pD_in_ga(T39, T43) → U4_ga(T39, T43, lessA_in_g(T39))
U4_ga(T39, T43, lessA_out_g(T39)) → pD_out_ga(T39, T43)
U4_ga(T39, T43, lessA_out_g(T39)) → U5_ga(T39, T43, insertC_in_gag(T39, T43, void))
insertC_in_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void)) → U10_gag(T57, T54, pB_in_ga(T57, T54))
U10_gag(T57, T54, pB_out_ga(T57, T54)) → insertC_out_gag(s(T57), tree(s(T57), void, T54), tree(s(T57), void, void))
insertC_in_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void)) → U11_gag(T71, T66, pB_in_ga(T71, T66))
U11_gag(T71, T66, pB_out_ga(T71, T66)) → insertC_out_gag(s(T71), tree(s(T71), T66, void), tree(s(T71), void, void))
insertC_in_gag(T80, tree(T80, void, T84), tree(T80, void, void)) → U12_gag(T80, T84, pD_in_ga(T80, T84))
U12_gag(T80, T84, pD_out_ga(T80, T84)) → insertC_out_gag(T80, tree(T80, void, T84), tree(T80, void, void))
insertC_in_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void)) → U13_gag(T96, T93, pB_in_ga(T96, T93))
U13_gag(T96, T93, pB_out_ga(T96, T93)) → insertC_out_gag(s(T96), tree(s(T96), void, T93), tree(s(T96), void, void))
insertC_in_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102)) → insertC_out_gag(T100, tree(T100, T101, T102), tree(T100, T101, T102))
insertC_in_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_gag(T118, T113, T111, T112, lessA_in_g(T118))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U14_gag(T118, T113, T111, T112, lessA_out_g(T118)) → U15_gag(T118, T113, T111, T112, insertC_in_gag(s(T118), T113, T112))
insertC_in_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_gag(T131, T133, T136, T135, lessA_in_g(T131))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U16_gag(T131, T133, T136, T135, lessA_out_g(T131)) → U17_gag(T131, T133, T136, T135, insertC_in_gag(T131, T136, T135))
insertC_in_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_gag(T152, T146, T149, T148, lessA_in_g(T152))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U18_gag(T152, T146, T149, T148, lessA_out_g(T152)) → U19_gag(T152, T146, T149, T148, insertC_in_gag(s(T152), T149, T148))
insertC_in_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → U20_gag(T170, T165, T163, T164, insertC_in_gag(0, T165, T164))
insertC_in_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_gag(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
lessF_in_gg(0, s(T189)) → lessF_out_gg(0, s(T189))
lessF_in_gg(s(0), s(s(T202))) → lessF_out_gg(s(0), s(s(T202)))
lessF_in_gg(s(s(0)), s(s(s(T215)))) → lessF_out_gg(s(s(0)), s(s(s(T215))))
lessF_in_gg(s(s(s(0))), s(s(s(s(T228))))) → lessF_out_gg(s(s(s(0))), s(s(s(s(T228)))))
lessF_in_gg(s(s(s(s(0)))), s(s(s(s(s(T241)))))) → lessF_out_gg(s(s(s(s(0)))), s(s(s(s(s(T241))))))
lessF_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254))))))) → lessF_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254)))))))
lessF_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267)))))))) → lessF_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267))))))))
lessF_in_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_gg(T272, T273, lessE_in_gg(T272, T273))
lessE_in_gg(0, s(T284)) → lessE_out_gg(0, s(T284))
lessE_in_gg(s(T289), s(T290)) → U6_gg(T289, T290, lessE_in_gg(T289, T290))
U6_gg(T289, T290, lessE_out_gg(T289, T290)) → lessE_out_gg(s(T289), s(T290))
U7_gg(T272, T273, lessE_out_gg(T272, T273)) → lessF_out_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273))))))))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U21_gag(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → U22_gag(T179, T180, T165, T163, T164, insertC_in_gag(s(T179), T165, T164))
insertC_in_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_gag(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U23_gag(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → U24_gag(T305, T306, T307, T310, T309, insertC_in_gag(T305, T310, T309))
insertC_in_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → U25_gag(T332, T324, T327, T326, insertC_in_gag(s(T332), T327, T326))
insertC_in_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_gag(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U26_gag(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → U27_gag(T340, T339, T324, T327, T326, insertC_in_gag(s(T340), T327, T326))
U27_gag(T340, T339, T324, T327, T326, insertC_out_gag(s(T340), T327, T326)) → insertC_out_gag(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326))
U25_gag(T332, T324, T327, T326, insertC_out_gag(s(T332), T327, T326)) → insertC_out_gag(s(T332), tree(0, T324, T327), tree(0, T324, T326))
U24_gag(T305, T306, T307, T310, T309, insertC_out_gag(T305, T310, T309)) → insertC_out_gag(T305, tree(T306, T307, T310), tree(T306, T307, T309))
U22_gag(T179, T180, T165, T163, T164, insertC_out_gag(s(T179), T165, T164)) → insertC_out_gag(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163))
U20_gag(T170, T165, T163, T164, insertC_out_gag(0, T165, T164)) → insertC_out_gag(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163))
U19_gag(T152, T146, T149, T148, insertC_out_gag(s(T152), T149, T148)) → insertC_out_gag(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148))
U17_gag(T131, T133, T136, T135, insertC_out_gag(T131, T136, T135)) → insertC_out_gag(T131, tree(T131, T133, T136), tree(T131, T133, T135))
U15_gag(T118, T113, T111, T112, insertC_out_gag(s(T118), T113, T112)) → insertC_out_gag(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111))
U5_ga(T39, T43, insertC_out_gag(T39, T43, void)) → pD_out_ga(T39, T43)
U9_gag(T39, T43, pD_out_ga(T39, T43)) → insertC_out_gag(T39, tree(T39, void, T43), tree(T39, void, void))
U3_ga(T25, T20, insertC_out_gag(s(T25), T20, void)) → pB_out_ga(T25, T20)
U8_gag(T25, T20, pB_out_ga(T25, T20)) → insertC_out_gag(s(T25), tree(s(T25), T20, void), tree(s(T25), void, void))
INSERTC_IN_GAG(s(T118), tree(s(T118), T113, T111), tree(s(T118), T112, T111)) → U14_GAG(T118, T113, T111, T112, lessA_in_g(T118))
U14_GAG(T118, T113, T111, T112, lessA_out_g(T118)) → INSERTC_IN_GAG(s(T118), T113, T112)
INSERTC_IN_GAG(T131, tree(T131, T133, T136), tree(T131, T133, T135)) → U16_GAG(T131, T133, T136, T135, lessA_in_g(T131))
U16_GAG(T131, T133, T136, T135, lessA_out_g(T131)) → INSERTC_IN_GAG(T131, T136, T135)
INSERTC_IN_GAG(s(T152), tree(s(T152), T146, T149), tree(s(T152), T146, T148)) → U18_GAG(T152, T146, T149, T148, lessA_in_g(T152))
U18_GAG(T152, T146, T149, T148, lessA_out_g(T152)) → INSERTC_IN_GAG(s(T152), T149, T148)
INSERTC_IN_GAG(s(T179), tree(s(T180), T165, T163), tree(s(T180), T164, T163)) → U21_GAG(T179, T180, T165, T163, T164, lessF_in_gg(T179, T180))
U21_GAG(T179, T180, T165, T163, T164, lessF_out_gg(T179, T180)) → INSERTC_IN_GAG(s(T179), T165, T164)
INSERTC_IN_GAG(T305, tree(T306, T307, T310), tree(T306, T307, T309)) → U23_GAG(T305, T306, T307, T310, T309, lessE_in_gg(T306, T305))
U23_GAG(T305, T306, T307, T310, T309, lessE_out_gg(T306, T305)) → INSERTC_IN_GAG(T305, T310, T309)
INSERTC_IN_GAG(0, tree(s(T170), T165, T163), tree(s(T170), T164, T163)) → INSERTC_IN_GAG(0, T165, T164)
INSERTC_IN_GAG(s(T332), tree(0, T324, T327), tree(0, T324, T326)) → INSERTC_IN_GAG(s(T332), T327, T326)
INSERTC_IN_GAG(s(T340), tree(s(T339), T324, T327), tree(s(T339), T324, T326)) → U26_GAG(T340, T339, T324, T327, T326, lessE_in_gg(T339, T340))
U26_GAG(T340, T339, T324, T327, T326, lessE_out_gg(T339, T340)) → INSERTC_IN_GAG(s(T340), T327, T326)
lessA_in_g(s(T28)) → U1_g(T28, lessA_in_g(T28))
lessF_in_gg(0, s(T189)) → lessF_out_gg(0, s(T189))
lessF_in_gg(s(0), s(s(T202))) → lessF_out_gg(s(0), s(s(T202)))
lessF_in_gg(s(s(0)), s(s(s(T215)))) → lessF_out_gg(s(s(0)), s(s(s(T215))))
lessF_in_gg(s(s(s(0))), s(s(s(s(T228))))) → lessF_out_gg(s(s(s(0))), s(s(s(s(T228)))))
lessF_in_gg(s(s(s(s(0)))), s(s(s(s(s(T241)))))) → lessF_out_gg(s(s(s(s(0)))), s(s(s(s(s(T241))))))
lessF_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254))))))) → lessF_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254)))))))
lessF_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267)))))))) → lessF_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267))))))))
lessF_in_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_gg(T272, T273, lessE_in_gg(T272, T273))
lessE_in_gg(0, s(T284)) → lessE_out_gg(0, s(T284))
lessE_in_gg(s(T289), s(T290)) → U6_gg(T289, T290, lessE_in_gg(T289, T290))
U1_g(T28, lessA_out_g(T28)) → lessA_out_g(s(T28))
U7_gg(T272, T273, lessE_out_gg(T272, T273)) → lessF_out_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273))))))))
U6_gg(T289, T290, lessE_out_gg(T289, T290)) → lessE_out_gg(s(T289), s(T290))
INSERTC_IN_GAG(s(T118), tree(s(T118), T112, T111)) → U14_GAG(T118, T112, lessA_in_g(T118))
U14_GAG(T118, T112, lessA_out_g) → INSERTC_IN_GAG(s(T118), T112)
INSERTC_IN_GAG(T131, tree(T131, T133, T135)) → U16_GAG(T131, T135, lessA_in_g(T131))
U16_GAG(T131, T135, lessA_out_g) → INSERTC_IN_GAG(T131, T135)
INSERTC_IN_GAG(s(T152), tree(s(T152), T146, T148)) → U18_GAG(T152, T148, lessA_in_g(T152))
U18_GAG(T152, T148, lessA_out_g) → INSERTC_IN_GAG(s(T152), T148)
INSERTC_IN_GAG(s(T179), tree(s(T180), T164, T163)) → U21_GAG(T179, T164, lessF_in_gg(T179, T180))
U21_GAG(T179, T164, lessF_out_gg) → INSERTC_IN_GAG(s(T179), T164)
INSERTC_IN_GAG(T305, tree(T306, T307, T309)) → U23_GAG(T305, T309, lessE_in_gg(T306, T305))
U23_GAG(T305, T309, lessE_out_gg) → INSERTC_IN_GAG(T305, T309)
INSERTC_IN_GAG(0, tree(s(T170), T164, T163)) → INSERTC_IN_GAG(0, T164)
INSERTC_IN_GAG(s(T332), tree(0, T324, T326)) → INSERTC_IN_GAG(s(T332), T326)
INSERTC_IN_GAG(s(T340), tree(s(T339), T324, T326)) → U26_GAG(T340, T326, lessE_in_gg(T339, T340))
U26_GAG(T340, T326, lessE_out_gg) → INSERTC_IN_GAG(s(T340), T326)
lessA_in_g(s(T28)) → U1_g(lessA_in_g(T28))
lessF_in_gg(0, s(T189)) → lessF_out_gg
lessF_in_gg(s(0), s(s(T202))) → lessF_out_gg
lessF_in_gg(s(s(0)), s(s(s(T215)))) → lessF_out_gg
lessF_in_gg(s(s(s(0))), s(s(s(s(T228))))) → lessF_out_gg
lessF_in_gg(s(s(s(s(0)))), s(s(s(s(s(T241)))))) → lessF_out_gg
lessF_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T254))))))) → lessF_out_gg
lessF_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T267)))))))) → lessF_out_gg
lessF_in_gg(s(s(s(s(s(s(s(T272))))))), s(s(s(s(s(s(s(T273)))))))) → U7_gg(lessE_in_gg(T272, T273))
lessE_in_gg(0, s(T284)) → lessE_out_gg
lessE_in_gg(s(T289), s(T290)) → U6_gg(lessE_in_gg(T289, T290))
U1_g(lessA_out_g) → lessA_out_g
U7_gg(lessE_out_gg) → lessF_out_gg
U6_gg(lessE_out_gg) → lessE_out_gg
lessA_in_g(x0)
lessF_in_gg(x0, x1)
lessE_in_gg(x0, x1)
U1_g(x0)
U7_gg(x0)
U6_gg(x0)
From the DPs we obtained the following set of size-change graphs: